DEF MAIN:bool == true

-- Test predefined Function calls
DEF add1(X:nat, Y:nat):nat == add(X,Y)
DEF mult1(X:nat, Y:nat):nat == mul(X,Y)
DEF eq1(X:nat, Y:nat):bool == eq(X,Y)
DEF and1(X:bool, Y:bool):bool == and(X, Y)
DEF sub1(X:nat, Y:nat):nat == sub(X, Y)
DEF div1(X:nat, Y:nat):nat == div(X, Y)
DEF lt1(X:nat, Y:nat):bool == lt(X, Y)
DEF or1(X:bool, Y:bool):bool == or(X, Y)
DEF not1(X:bool):bool == not(X)

-- Test Redefinition of predefined Functions
DEF add(X:nat, Y:nat):nat == add(X,Y)
DEF mul(X:nat, Y:nat):nat == mul(X,Y)
DEF eq(X:nat, Y:nat):bool == eq(X,Y)
DEF and(X:bool, Y:bool):bool == and(X, Y)
DEF sub(X:nat, Y:nat):nat == sub(X, Y)
DEF div(X:nat, Y:nat):nat == div(X, Y)
DEF lt(X:nat, Y:nat):bool == lt(X, Y)
DEF or(X:bool, Y:bool):bool == or(X, Y)
DEF not(X:bool):bool == not(X)

